/LMAR=0/XLINE=3/FONT#0=BAXL30/FONT#1=BAXM30/FONT#2=BASB30/FONT#3=SUB/FONT#4=SUP/FONT#5=BASL35/FONT#6=NGR25/FONT#7=MATH30/FONT#8=FIX25/FONT#9=GRKB30/FONT#10=ZERO30
␈↓ α∧␈↓␈↓ u1


␈↓ α∧␈↓α␈↓ ∧|AN INTERESTING LISP FUNCTION

␈↓ α∧␈↓␈↓ αTIkuo␈α⊃Takeuchi␈α⊃of␈α⊃the␈α⊃Electrical␈α⊃Communication␈α⊃Laboratory␈α⊃of␈α⊃Nippon␈α⊃Telephone␈α⊃and
␈↓ α∧␈↓Telegraph␈α∃Co.␈α∃(Japan's␈α∃Bell␈α∃Labs)␈α∃devised␈α∃a␈α∃recursive␈α∃function␈α∃program␈α∃for␈α∃testing␈α∃and
␈↓ α∧␈↓comparing␈αLISP␈αsystems.␈α Its␈αvirtue␈αis␈αthat␈αit␈αtakes␈αa␈αlong␈αtime␈αto␈αrun␈αbut␈αdoesn't␈αgenerate␈αlarge
␈↓ α∧␈↓numbers or use much stack.  The program is

␈↓ α∧␈↓␈↓ αT␈↓↓tak(x, y, z) ← ␈↓αif␈↓↓ x ≤ y ␈↓αthen␈↓↓ y ␈↓αelse␈↓↓ tak(tak(x - 1, y, z), tak(y - 1, z, x), tak(z - 1, x, y))␈↓,

␈↓ α∧␈↓where␈α
the␈α
variables␈α
may␈α
range␈α
over␈α
the␈α
integers␈α
(including␈α
negative)␈α
or␈α
else␈α
over␈α
real␈α
numbers.
␈↓ α∧␈↓The␈α	program␈α
has␈α
similar␈α
properties␈α
in␈α
the␈α
two␈α
cases,␈α
but␈α
some␈α
of␈α	the␈α
proofs␈α
seem␈α
more␈α
difficult␈α
in
␈↓ α∧␈↓the real case.  The program has several interesting features.

␈↓ α∧␈↓␈↓ αT1. Inspection suggests that the function satisfies the equation

␈↓ α∧␈↓␈↓ αT␈↓↓tak(x + a, y + a, z + a) = tak(x, y, z) + a␈↓,

␈↓ α∧␈↓whenever␈α
the␈α
computation␈α
terminates,␈α
and␈α
this␈α
follows␈α
by␈α
subgoal␈α
induction.␈α
 Namely,␈α
it␈α
is␈α
true
␈↓ α∧␈↓for␈α∞the␈α∞non-recursive␈α∞case,␈α∞and␈α∞assuming␈α∞it␈α∞for␈α∞the␈α∞referred␈α∞sets␈α∞of␈α∞arguments␈α∞yields␈α∞it␈α∞for␈α∞the
␈↓ α∧␈↓main set.  A formal proof proceeds as in (McCarthy 1978).

␈↓ α∧␈↓␈↓ αT2.␈αExperiment␈αusing␈αLISP␈αindicates␈αfirst␈αof␈αall␈αthat␈αthe␈αvalue␈αof␈α␈↓↓tak(x, y, z)␈↓␈αis␈αalways␈αone
␈↓ α∧␈↓of ␈↓↓x,␈↓ ␈↓↓y␈↓ or ␈↓↓z.␈↓ I don't see a proof of this fact in isolation.

␈↓ α∧␈↓␈↓ αT3.␈α⊂Like␈α⊂the␈α⊂91-function,␈α⊂the␈α⊂program␈α⊂computes␈α⊂a␈α⊂simple␈α⊂non-recursive␈α⊂function.␈α⊂ Using
␈↓ α∧␈↓LISP to compute some values of ␈↓↓tak␈↓ quickly leads to the guess that it is the same as

␈↓ α∧␈↓␈↓ αT␈↓↓tak0(x,y,z) = ␈↓αif␈↓↓ x ≤ y ␈↓αthen␈↓↓ y ␈↓αelse␈↓↓ ␈↓αif␈↓↓ y ≤ z ␈↓αthen␈↓↓ z ␈↓αelse␈↓↓ x␈↓.

␈↓ α∧␈↓Subsititution␈α⊂shows␈α⊂that␈α⊂␈↓↓tak0␈↓␈α⊂satisfies␈α⊂the␈α⊂functional␈α⊂equation␈α⊂for␈α⊂␈↓↓tak,␈↓␈α⊂and␈α⊂therefore␈α⊂by␈α⊂the
␈↓ α∧␈↓␈↓↓minimization schema␈↓ of (McCarthy 1978),

␈↓ α∧␈↓␈↓ αT␈↓↓tak(x, y, z) = tak0(x, y, z)␈↓

␈↓ α∧␈↓whenever␈α∂the␈α∂former␈α∂terminates.␈α∂ ␈↓↓A␈α∂fortiori␈↓,␈α∂this␈α∂establishes␈α∂that␈α∂␈↓↓tak(x, y, z)␈↓␈α∂takes␈α∂one␈α∂of␈α∂the
␈↓ α∧␈↓variables as value, but maybe it could be proved separately.

␈↓ α∧␈↓␈↓ αT4. We now want to prove that ␈↓↓tak␈↓ is total, and we proceed as follows:

␈↓ α∧␈↓First,␈α
we␈α
write␈α
a␈α
␈↓↓"derived␈α
program"␈α
dtak(x, y, z)␈↓␈α
that␈α
computes␈α
the␈α
depth␈α
of␈α
recursion␈α
involved␈α
in
␈↓ α∧␈↓computing ␈↓↓tak(x, y, z)␈↓ using call-by-value.  We have

␈↓ α∧␈↓␈↓ αT␈↓↓dtak(x, y, z) ← ␈↓αif␈↓↓ x ≤ y ␈↓αthen␈↓↓ 0 ␈↓αelse␈↓↓ 1 + max(
␈↓ α∧␈↓␈↓↓␈↓ ¬Tdtak(x - 1, y, z),
␈↓ α∧␈↓↓␈↓ ¬Tdtak(y - 1, x, z),
␈↓ α∧␈↓↓␈↓ ¬Tdtak(z - 1, x, y),
␈↓ α∧␈↓↓␈↓ ¬Tdtak(tak(x - 1, y, z), tak(y - 1, z, x), tak(z - 1, x, y)))␈↓.

␈↓ α∧␈↓Empirical␈α∃study␈α∃leads␈α∃to␈α∃the␈α∃conjecture␈α∃that␈α∃for␈α∃integer␈α∃values␈α∃of␈α∃the␈α∃variables,␈α∃␈↓↓dtak␈↓␈α∃is
␈↓ α∧␈↓extensionally equivalent to
␈↓ α∧␈↓␈↓ u2


␈↓ α∧␈↓␈↓ αT␈↓↓dtak0(x,y,z) = dtak00(x - y, z - y)␈↓,

␈↓ α∧␈↓where

␈↓ α∧␈↓␈↓ αT␈↓↓dtak00(m,n) =␈↓ ∧$␈↓αif␈↓↓ m ≤ 0 ␈↓αthen␈↓↓ 0
␈↓ α∧␈↓␈↓↓␈↓ ∧$␈↓αelse␈↓↓ ␈↓αif␈↓↓ n ≥ 2 ␈↓αthen␈↓↓ m + n(n - 1)/2 -1
␈↓ α∧␈↓↓␈↓ ∧$␈↓αelse␈↓↓ ␈↓αif␈↓↓ n ≥ 0 ␈↓αthen␈↓↓ m
␈↓ α∧␈↓↓␈↓ ∧$␈↓αelse␈↓↓ ␈↓αif␈↓↓ n = -1 ␈↓αthen␈↓↓ (m + 1)(m + 2)/2 - 1
␈↓ α∧␈↓↓␈↓ ∧$␈↓αelse␈↓↓ (m - n)(m - n + 1)/2 - m - 1␈↓.

␈↓ α∧␈↓␈↓ αTWe␈α
don't␈α
bother␈α
to␈α
verify␈α
the␈α
conjecture.␈α
 Instead␈α
we␈α
use␈α
␈↓↓dtak0␈↓␈α
as␈α
a␈α
rank␈α
function␈α
to␈α
prove
␈↓ α∧␈↓␈↓↓∀i.␈↓	F␈↓↓(i)␈↓ by course-of-values induction where

␈↓ α∧␈↓␈↓ αT␈↓↓␈↓	F␈↓↓(i) ≡ ∀x y z.(dtak0(x, y, z) = i ⊃ tak(x, y, z) = tak0(x, y, z))␈↓.

␈↓ α∧␈↓In order to prove this we must show that

␈↓ α∧␈↓␈↓ αT␈↓↓∀x y z.(x > y ⊃
␈↓ α∧␈↓␈↓↓␈↓ βDdtak0(x - 1, y, z) < dtak0(x, y, z)
␈↓ α∧␈↓↓␈↓ βD∧ dtak0(y - 1, z, x) < dtak0(x, y, z)
␈↓ α∧␈↓↓␈↓ βD∧ dtak0(z - 1, x, y) < dtak0(x, y, z)
␈↓ α∧␈↓↓␈↓ βD∧ dtak0(tak0(x - 1, y, z), tak0(y - 1, z, x), tak0(z - 1, x, y)) < dtak0(x, y, z))␈↓.

␈↓ α∧␈↓Each␈αof␈αthe␈αfour␈αinequalities␈αfollows␈αfrom␈αa␈αseparate␈αeasy␈αcase␈αanalysis.␈α Presumably␈αtermination
␈↓ α∧␈↓could␈α
be␈αproved␈αfor␈αthe␈αnon-integer␈αcase␈αby␈αa␈αsimilar␈αargument␈α
with␈αa␈αmore␈αcomplicated␈αformula
␈↓ α∧␈↓for ␈↓↓dtak00.␈↓ We leave this as an exercise for the reader.

␈↓ α∧␈↓␈↓ αT5. Like Morris's program

␈↓ α∧␈↓␈↓ αT␈↓↓morris(x,y) ← ␈↓αif␈↓↓ x = 0 ␈↓αthen␈↓↓ 1 ␈↓αelse␈↓↓ morris(x - 1, morris(x, y))␈↓,

␈↓ α∧␈↓␈↓↓tak␈↓␈α
is␈α
more␈α
quickly␈α
computed␈α
by␈α
call-by-need.␈α
 In␈α
fact␈α
the␈α
number␈α
of␈α
function␈α
calls␈α
appears␈α
to␈α
be
␈↓ α∧␈↓exponential␈α∃with␈α∃call-by-value␈α∃and␈α∃quadratic␈α∃with␈α∀call-by-need.␈α∃ The␈α∃culprit␈α∃is␈α∃the␈α∃third
␈↓ α∧␈↓argument␈α⊂of␈α⊂the␈α⊂outer␈α⊂call,␈α⊂namely␈α⊂␈↓↓tak(z - 1, x, y)␈↓␈α⊂which␈α⊂is␈α⊂often␈α⊂unneeded.␈α⊂ Unlike␈α⊂␈↓↓morris,␈↓
␈↓ α∧␈↓however, ␈↓↓tak␈↓ is total.

␈↓ α∧␈↓␈↓ αTA call-by-need version of ␈↓↓tak␈↓ is given by

␈↓ α∧␈↓␈↓ αT␈↓↓ntak(x, y, z) ← vtak <x, y, z>␈↓

␈↓ α∧␈↓where

␈↓ α∧␈↓␈↓ αT␈↓↓vtak u ←␈↓ βd␈↓αif␈↓↓ numberp u ␈↓αthen␈↓↓ u
␈↓ α∧␈↓␈↓↓␈↓ βd␈↓αelse␈↓↓ ␈↓αif␈↓↓ ␈↓αn␈↓↓ ␈↓αd␈↓↓ u ␈↓αthen␈↓↓ vtak(␈↓αa␈↓↓ u) - 1
␈↓ α∧␈↓↓␈↓ βd␈↓αelse␈↓↓ {vtak ␈↓αa␈↓↓ u, vtak ␈↓αad␈↓↓ u}[λx y.
␈↓ α∧␈↓↓␈↓ ¬T␈↓αif␈↓↓ x ≤ y ␈↓αthen␈↓↓ y
␈↓ α∧␈↓↓␈↓ ¬T␈↓αelse␈↓↓ vtak <␈↓ εd<x - 1, y, ␈↓αadd␈↓↓ u>,
␈↓ α∧␈↓↓␈↓ εd<y - 1, ␈↓αadd␈↓↓ u, x>,
␈↓ α∧␈↓↓␈↓ εd<␈↓αadd␈↓↓ u - 1, x, y>>]␈↓.
␈↓ α∧␈↓␈↓ u3


␈↓ α∧␈↓␈↓↓vtak␈↓␈α∩is␈α∩obtained␈α∩from␈α∩␈↓↓tak␈↓␈α∩in␈α∩a␈α∩somewhat␈α∩ad␈α∩hoc␈α∩way.␈α∩ Since␈α∩we␈α∩don't␈α∩always␈α∩compute␈α∩all
␈↓ α∧␈↓arguments␈α∪of␈α∪a␈α∪function␈α∪we␈α∪must␈α∩work␈α∪with␈α∪triples␈α∪whose␈α∪elements␈α∪are␈α∪either␈α∪numbers␈α∪or
␈↓ α∧␈↓applications␈α∪of␈α∪functions␈α∪to␈α∪arguments.␈α∪ The␈α∪only␈α∪functions␈α∪that␈α∪occur␈α∪are␈α∪␈↓↓vtak␈↓␈α∪itself␈α∪and
␈↓ α∧␈↓subtracting␈αone.␈α Therefore,␈αa␈αnumber␈αstands␈αfor␈αitself,␈αan␈αapplication␈αof␈α␈↓↓vtak␈↓␈αis␈αrepresented␈αby␈αa
␈↓ α∧␈↓triple,␈α
and␈α
an␈α
application␈α
of␈α
subtracting␈α
one␈α
is␈α
represented␈α
by␈α
a␈α
list␈α
of␈α
one␈α
element␈α
-␈α
the␈α
inner
␈↓ α∧␈↓expression␈αfrom␈αwhich␈αone␈αis␈αto␈αbe␈αsubtracted.␈α Perhaps␈αI'm␈αbeing␈αthick,␈αbut␈αit␈αseems␈αto␈αme␈αthat
␈↓ α∧␈↓call-by-need requires lists or at least putting symbols on the stack.

␈↓ α∧␈↓␈↓ αTLISP␈α
versions␈α
of␈α
␈↓↓tak␈↓␈α
and␈α
many␈α
of␈α
its␈α
friends␈α
are␈α
in␈α
the␈α
file␈α
TAK.LSP[E78,JMC]␈α
at␈α
SU-AI.
␈↓ α∧␈↓I␈αthank␈αDon␈αKnuth␈αfor␈αsuggesting␈αcall-by-need.␈α The␈αexternal␈αor␈αpublication␈αLISP␈αnotation␈αis␈αas
␈↓ α∧␈↓in (McCarthy and Talcott 1978).

␈↓ α∧␈↓John McCarthy
␈↓ α∧␈↓Artificial Intelligence Laboratory
␈↓ α∧␈↓Computer Science Department
␈↓ α∧␈↓Stanford University
␈↓ α∧␈↓Stanford, California 94305

␈↓ α∧␈↓ARPANET: MCCARTHY@SU-AI

␈↓ α∧␈↓␈↓εThis version of TAKEUC[E78,JMC] translated for printing (by PUB) at 16:29 on January 10, 1986.␈↓